(module equal-types (lib "eopl.ss" "eopl")

  (provide equal-types?)

  (define equal-types?
    (lambda (ty1 ty2)
      (equal-up-to-gensyms? ty1 ty2)))

  ;; equal-up-to-gensyms? : sexp * sexp -> (optional alist)

  ;; checks to see if two list structures differ
  ;; only up to gensym'd type variables.  Builds a table to make sure
  ;; the renaming is consistent, and if so, returns it, else returns #f

  ;; sexp = symbol | (list-of sexp)
  ;; alist = (list (pair tvar-sym tvar-sym))
  ;; a tvar-sym is a symbol ending with a digit.

  (define equal-up-to-gensyms?
    (lambda (sexp1 sexp2)
      ;; loop : sexp * list * alist -> (optional alist)
      ;; takes two list and a partial correspondence of gensyms, and
      ;; returns either a bigger correspondence or #f
      (let loop ((sexp1 sexp1) (sexp2 sexp2) (table '()))
        (cond
          ((and (null? sexp1) (null? sexp2)) table)
          ((eqv? sexp1 sexp2) table)
          ((and (tvar-sym? sexp1) (tvar-sym? sexp2))
           ;; (printf "point a: sexp1 = ~s sexp2 = ~s ~%" sexp1 sexp2)
           (cond
             ;; is sexp1 already bound?  If so, make sure sexp2 matches
             ;; what's in the table.
             ((assq sexp1 table) => 
              (lambda (p)
                (if (eqv? (cdr p) sexp2)
                  table
                  #f)))
             ;; is sexp2 already the binding of some other tvar in the
             ;; table?  If so, we can't bind sexp1 to it.
             ((memq sexp2 (map cdr table)) #f)
             (else (cons (cons sexp1 sexp2) table))))
          ((and (pair? sexp1) (pair? sexp2))
           (cond 
             ((loop (car sexp1) (car sexp2) table)
              =>
              (lambda (table) (loop (cdr sexp1) (cdr sexp2) table)))
             (else #f)))
          (else #f)))))

  ;; the external representation of a tvar sym or a gensym'd module is
  ;; tvar%NNN or name%NNN.
  (define tvar-sym?
    (lambda (sym)
      (and (symbol? sym)
        (let ((chars-reversed
                (reverse (symbol->list sym))))
          (let loop ((chars chars-reversed))
            ;; is chars of the form (numeric)* . "%" ??
            (cond
              ((null? chars) #f)
              ((eqv? (car chars) #\%) #t)
              ((char-numeric? (car chars)) (loop (cdr chars)))
              (else #f)))))))

  (define symbol->list
    (lambda (x) (string->list (symbol->string x))))

  )